package common.correspondence;

import common.Announcement;
import common.CIBIO;
import common.proto.out.CountMessage;
import jdd.bdd.BDD;

import java.util.*;

public class BDDIOTransfer extends BDDTransferAbstract implements BDDTransfer{
    final BDD manager;

    public BDDIOTransfer(BDD manager){
        this.manager = manager;
    }

    public int[] bddToArray(int bdd){
        int count = manager.nodeCount(bdd);
        int[] res = new int[count*4+1];
        res[0] = bdd;
        synchronized (manager){
            recursiveSaveInArray(res, 1, bdd);
            manager.unmark_tree(bdd);
        }

        if(!manager.isValid(bdd)){
            System.err.println(bdd);
        }
        return res;
    }

    public void bddsToArray(Iterable<Integer> bdds, CountMessage.CountResult.Builder builder){
//        int count = manager.nodeCount(bdd);
//        List<Integer> res = new LinkedList<>();
        Set<Integer> markSet = new HashSet<>();

        for(Integer bdd:bdds) {
            recursiveSaveInArray(builder, bdd, markSet);
        }

//        System.out.println(res.size());
//        return res;
    }

    public String bddToString(int bdd) {
        StringBuilder sb = new StringBuilder();
        sb.append(bdd).append(" ");
        synchronized (manager){
            recursive_save(sb, bdd);
            manager.unmark_tree(bdd);
        }
        String s = sb.toString();

        if(!manager.isValid(bdd)){
            System.err.println(bdd);
        }
        return s;
    }

    public void recursiveSaveInArray(CountMessage.CountResult.Builder arr, int bdd, Set<Integer> markSet){
        if(bdd >= 2 && !markSet.contains(bdd)){
            markSet.add(bdd);
            int var = manager.getVarUnmasked(bdd);
            int low = manager.getLow(bdd);
            int high = manager.getHigh(bdd);
            recursiveSaveInArray(arr, low, markSet);
            recursiveSaveInArray(arr,high, markSet);
            arr.addNodeTree(bdd);
            arr.addNodeTree(var);
            arr.addNodeTree(low);
            arr.addNodeTree(high);
        }
    }

    public int recursiveSaveInArray(int[] arr, int index, int bdd){
        if(bdd >= 2 && !manager.isNodeMarked(bdd)){
            manager.mark_node(bdd);
            int var = manager.getVarUnmasked(bdd);
            int low = manager.getLow(bdd);
            int high = manager.getHigh(bdd);
            index = recursiveSaveInArray(arr, index, low);
            index = recursiveSaveInArray(arr, index, high);
            arr[index++] = bdd;
            arr[index++] = var;
            arr[index++] = low;
            arr[index++] = high;
        }
        return index;
    }


    private void recursive_save(StringBuilder sb, int bdd){
        if(bdd < 2) return;
        if(! manager.isNodeMarked(bdd)){

            manager.mark_node(bdd);

            int var = manager.getVarUnmasked(bdd);
            int low = manager.getLow(bdd);
            int high = manager.getHigh(bdd);

            recursive_save(sb, low);
            recursive_save(sb, high);

            sb.append(bdd).append(" ").append(var).append(" ").append(low).append(" ").append(high).append(" ");
        }
    }
    public void cibIOPredicateParse(List<Integer> arr, CIBIO cibio){

        Iterator<Integer> is = arr.iterator();
        int curr_vars = manager.numberOfVariables();
        Map<Integer, Integer> map = new HashMap<>();
        int ret;
        map.put(0, 0);
        map.put(1, 1);
        while (is.hasNext()) {
            int name = loadInt(is);
            int var  = loadInt(is);
            int low  = loadInt(is);
            int high = loadInt(is);

            Integer tmp = map.get(low);
            low = tmp;

            tmp = map.get(high);
            high = tmp;
            synchronized (manager) {
                if(var >= curr_vars) var = curr_vars-1;
                ret = manager.ref( manager.mk( var, low, high) );
            }
            map.put(name, ret);
        }

        for(Announcement a: cibio.announcements){
            a.predicate = manager.ref(map.get(a.predicate));
        }

        cibio.packetSpace = manager.ref(map.get(cibio.packetSpace));


        for (Integer i : map.values()) {
            manager.deref(i);
        }
    }
    public int arrayToBdd(int[] arr){

        Iterator<Integer> is = Arrays.stream(arr).iterator();

        int curr_vars = manager.numberOfVariables();
        int target = loadInt(is);
        Map<Integer, Integer> map = new HashMap<>();
        int ret;

        map.put(0, 0);
        map.put(1, 1);


        while (is.hasNext()) {
            int name = loadInt(is);
            int var  = loadInt(is);
            int low  = loadInt(is);
            int high = loadInt(is);

            Integer tmp = map.get(low);
            low = tmp;

            tmp = map.get(high);
            high = tmp;
            synchronized (manager) {
                while (var >= curr_vars) {
                    manager.createVar();
                    curr_vars++;
                }
                ret = manager.ref( manager.mk( var, low, high) );
            }
            map.put(name, ret);
        }

        ret = map.get(target);
        manager.ref(ret);

        for (Integer i : map.values()) {
            manager.deref(i);
        }

        return ret;
    }

    public int stringToBdd(String str) {
        return stringToBdd(Arrays.asList(str.split("\\s")));
    }

    // already ref
    public int stringToBdd(Iterable<String> str) {
        Iterator<String> is = str.iterator();

        int curr_vars = manager.numberOfVariables();
        int target = load_int(is);
        Map<Integer, Integer> map = new HashMap<>();
        int ret;

        map.put(0, 0);
        map.put(1, 1);


        while (is.hasNext()) {
            int name = load_int(is);
            int var  = load_int(is);
            int low  = load_int(is);
            int high = load_int(is);


            Integer tmp = map.get(low);
            low = tmp;

            tmp = map.get(high);
            high = tmp;
            synchronized (manager) {
                while (var >= curr_vars) {
                    manager.createVar();
                    curr_vars++;
                }
                ret = manager.ref( manager.mk( var, low, high) );
            }
            map.put(name, ret);
        }
        if(!map.containsKey(target))
            System.out.println(str);

        ret = map.get(target);
        manager.ref(ret);

        for (Integer i : map.values()) {
            manager.deref(i);
        }

        return ret;
    }



    private int load_int(Iterator<String> s){
        return Integer.parseInt(s.next());
    }
    private int loadInt(Iterator<Integer> s){
        return s.next();
    }

    private static int randomBDD(BDD bdd, Random random, int maxAnd){
        int res = 1;
        int andTime = maxAnd;
        for(int i=0;i<andTime;i++){
            int t = randomDstIPBDD(bdd, random.nextInt(32)+1, random);
            res = bdd.andTo(res, t);
            bdd.deref(t);
        }
        return res;
    }

    private static int randomDstIPBDD(BDD bdd, int n, Random random){
        int last = 1;
        for(int i=32;i<n+32;i++){
            int t;
            if(random.nextBoolean())
                t = bdd.ref(bdd.mk(i, 0, last));
            else
                t = bdd.ref(bdd.mk(i, last, 0));
            bdd.deref(last);
            last = t;
        }
        return last;
    }
}
